{-# LANGUAGE TypeFamilies, TypeOperators, QuasiQuotes #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

module Examples.Zippers where

import Data.Yoko.Zipper
import Data.Yoko.ZipperHelp

import Examples.TermBase
import qualified Examples.TermGeneric as G
import qualified Examples.Prelude as G

-- [(0, 'n'), (1, 'i'), (_, 'c'), (3, 'k')]
z0 :: Cxt [(Int, Char)] (In1 :< In2 :< Top)
z0 = in1 ([(1, 'i'), (0, 'n')], [(3, 'k')]) (in2 'c' Top)

-- Var _
z1 = inDC dc1 Top
dc1 = dcBase G.Var_ U U

-- z1 :: Cxt Term (InDC (Fd G.Var Z) :< Top)
-- dc1 :: CxtDC Term (Fd G.Var Z)

-- App (Var _) (Var 0)
-- dc2 :: CxtDC Term (InDC (Fd G.App Z) :< Top) (Fd G.Var Z)
dc2 = dcStep (inDC (dcBase G.App_ U (Var 0 :* U)) Top) $
      dc1

-- App (Var 0) (Var _)
-- dc3 :: CxtDC Term (InDC (Fd G.App (S Z)) :< Top) (Fd G.Var Z)
dc3 = dcStep (inDC (dcBase G.App_ (Var 0 :* U) U) Top) $
      dc1

-- Decl TBool (Var _)
-- dc4 :: CxtDC Decl (InDC (Fd G.Decl (S Z)) :< Top) (Fd G.Var Z)
dc4 = dcStep (inDC (dcBase G.Decl_ (TBool :* U) U) Top) $
      dc1

-- [Decl TInt (Var 1), _]
-- c5 :: Cxt [Decl] (In1 :< Top)
c5 = in1_ qList ([Decl TInt (Var 1)], []) Top

qList :: Proxy ([qK|*->*|] [])
qList = Proxy

-- Let [Decl TInt (Var 1), _] (Var 0)
-- c6 :: Cxt Term (InDC ((Fd G.Let Z)) :< In1 :< Top)
c6 = inDC (dcBase G.Let_ U (Var 0 :* U)) c5

-- Let [Decl TInt (Var 1), Decl TBool (Var _)] (Var 0)
-- dc7 :: CxtDC Term (Fd G.Var Z)
-- dc7 :: CxtDC Term (InDC ((Fd G.Let Z)) :< InDC (Fd G.Decl (S Z)) :< Top) (Fd G.Var Z)
dc7 = dcStep c6 dc4

-- dc7' :: CxtDC Term (InDC ((Fd G.Let Z)) :< (InDC (Fd G.Decl (S Z)) :< Top)) (Fd G.Var Z)
dc7' = dcStep (inDC (dcBase G.Lam_ (TInt :* U) U) Top) $
       dcStep (inDC (dcBase G.Let_ U (Var 0 :* U)) $
               in1_ qList ([Decl TInt (Var 1)], []) $
               Top) $
       dcStep (inDC (dcBase G.Decl_ (TBool :* U) U) Top) $
       dcBase G.Var_ U U

-- PROHIBITED by CxtDC_Step's NoRs constraint
-- baddc7' :: CxtDC Term (InDC (Fd G.Lam (S Z)) :< (InDC (Fd G.Decl (S Z)) :< Top)) (Fd G.Var Z)
{-baddc7' = 
       dcStep (inDC (dcBase G.Lam_ (TInt :* U) U) $
               inDC (dcBase G.Let_ U (Var 0 :* U)) $
               in1_ qList ([Decl TInt (Var 1)], []) $
               Top) $
       dcStep (inDC (dcBase G.Decl_ (TBool :* U) U) Top) $
       dcBase G.Var_ U U-}

-- z8 :: Zip Term (InDC (Fd G.Var Z) :< Top)
z8 = Zip 2 $ inDC dc7 Top

-- INFINITE LIST
-- z9 :: Zip String (InDC (Fd (G.Cons Char) Z) :< Top)
z9 = Zip 'c' $ inDC (dcBase G.Cons_ U (top z9 :* U)) Top
